ap2(f, x) -> x
ap2(ap2(ap2(g, x), y), ap2(s, z)) -> ap2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
↳ QTRS
↳ DependencyPairsProof
ap2(f, x) -> x
ap2(ap2(ap2(g, x), y), ap2(s, z)) -> ap2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(x, y)
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(ap2(x, y), 0)
ap2(f, x) -> x
ap2(ap2(ap2(g, x), y), ap2(s, z)) -> ap2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(x, y)
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(ap2(x, y), 0)
ap2(f, x) -> x
ap2(ap2(ap2(g, x), y), ap2(s, z)) -> ap2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(x, y)
ap2(f, x) -> x
ap2(ap2(ap2(g, x), y), ap2(s, z)) -> ap2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(x, y)
Used ordering: Polynomial Order [17,21] with Interpretation:
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
POL( AP2(x1, x2) ) = max{0, x1 - 3}
POL( ap2(x1, x2) ) = x1 + x2 + 1
POL( g ) = 2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
ap2(f, x) -> x
ap2(ap2(ap2(g, x), y), ap2(s, z)) -> ap2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))